g:OGrp. (ghgrp)  GrpSig 

latex

Up	groups 1
Definitions of Statement	GrpSig, |g|, =, , *, e, Mon, AbMon, OCMon, OGrp, |g|, ghgrp
Definitions	suptype(S; T), S  T, ghgrp, GrpSig, t  T, x:A. B(x), Mon, AbMon, OCMon, |g|, OGrp
Lemmas	ocgrp wf, grp id wf2, grp op wf2, grp le wf, grp car wf, bool wf, grp eq wf, hgrp car wf